Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(x1))) → a(b(b(a(x1))))
b(b(b(x1))) → b(b(x1))
Q is empty.
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
a(b(a(x1))) → a(b(b(a(x1))))
b(b(b(x1))) → b(b(x1))
Q is empty.
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → A(b(b(a(x1))))
A(b(a(x1))) → B(b(a(x1)))
The TRS R consists of the following rules:
a(b(a(x1))) → a(b(b(a(x1))))
b(b(b(x1))) → b(b(x1))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → A(b(b(a(x1))))
A(b(a(x1))) → B(b(a(x1)))
The TRS R consists of the following rules:
a(b(a(x1))) → a(b(b(a(x1))))
b(b(b(x1))) → b(b(x1))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ RFCMatchBoundsDPProof
Q DP problem:
The TRS P consists of the following rules:
A(b(a(x1))) → A(b(b(a(x1))))
The TRS R consists of the following rules:
a(b(a(x1))) → a(b(b(a(x1))))
b(b(b(x1))) → b(b(x1))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
Finiteness of the DP problem can be shown by a matchbound of 1.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:
A(b(a(x1))) → A(b(b(a(x1))))
To find matches we regarded all rules of R and P:
a(b(a(x1))) → a(b(b(a(x1))))
b(b(b(x1))) → b(b(x1))
A(b(a(x1))) → A(b(b(a(x1))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
54, 55, 57, 58, 56, 60, 61, 59
Node 54 is start node and node 55 is final node.
Those nodes are connect through the following edges:
- 54 to 56 labelled A_1(0)
- 55 to 55 labelled #_1(0)
- 57 to 58 labelled b_1(0)
- 58 to 55 labelled a_1(0)
- 58 to 59 labelled a_1(1)
- 56 to 57 labelled b_1(0)
- 60 to 61 labelled b_1(1)
- 61 to 55 labelled a_1(1)
- 61 to 59 labelled a_1(1)
- 59 to 60 labelled b_1(1)